% por Laski y Mata 
\begin{problema}{procesarComandoG}{g: Gateway, u: Usuario, r: SMS}{SMS}
	\requiere{(\exists t \selec trivias(g)) u \in partipantes(t)}
	\requiere{(\exists c \selec comandos(g)) c==damePalabras(texto(r))_0}
	\requiere{nroDestino(r) == numero (g)}
	
	\medskip
	
	\modifica g
	
	\medskip
	\asegura{procesarComandoAux(g,pre(g),u,r,result)}
\end{problema}


\begin{aux}{procesarComandoAux}{g,preg: Gateway, u: Usuario, r,result:SMS}{Bool}{\\
    nroDestino(result) == u \\ 
	\ylogico (loDemasNoCambiaG(g,preg))\\
	\ylogico (\longitud {trivias(g)} == \longitud {trivias(preg)})\\
	\ylogico (noTeEntiendo(r,preg,u) \implica ((texto(result)==\!''No\ te\
	entiendo'') \ylogico (mismos(trivias(g),trivias(preg)))))\\
	\ylogico (bajaTotal(r) \implica OkBajaTotal(g,preg,u,result))\\
	\ylogico (bajaTrivia(r,preg,u) \implica
	OkBajaTrivia(g,preg,damePalabras(texto(r))_1,u,result))\\ \ylogico
	(rankingTrivia(r,preg,u) \implica
	OkRankingTrivia(g,preg,damePalabras(texto(r))_1,u,result)) }
\end{aux}

\medskip

\begin{aux}{bajaTotal}{r: SMS}{Bool}{ \\
(\longitud {damePalabras(texto(r))} == 1) \\ 
\ylogico (damePalabras(texto(r))_0 = \!''BAJA'') 
}
\end{aux}

\medskip
	
\begin{aux}{bajaTrivia}{r:SMS, preg:Gateway, u:Usuario}{Bool}{\\
(\longitud {damePalabras(texto(r))} == 2) \\ \ylogico 
(damePalabras(texto(r))_0 = \!''BAJA'') \\ \ylogico
(\exists t \selec trivias(preg))((\exists k \selec keywords(t))
(damePalabras(texto(r))_1 == k)) \ylogico (u \in participantes(t)) }
\end{aux}

\medskip

\begin{aux}{rankingTrivia}{r:SMS, preg:Gateway, u: Usuario}{Bool}{\\
(\longitud {damePalabras(texto(r))} == 2) \\ 
\ylogico (damePalabras(texto(r))_0 = \!''RANKING'') \\ \ylogico
(\exists t \selec trivias(preg)) (damePalabras(texto(r))_1 \in keywords(t))
\ylogico (u \in participantes(t))}
\end{aux}

\medskip

\begin{aux}{noTeEntiendo}{r:SMS, preg:Gateway, u:Usuario}{Bool}{\\
\neg (bajaTotal(r)) \ylogico \neg (bajaTrivia(r,preg,u)) \ylogico
\neg (rakingTrivia(r,preg,u)) }
\end{aux}

\medskip

\begin{aux}{OkBajaTotal}{g,preg:Gateway, u:Usuario, result:SMS}{Bool}{\\
(\forall k \selec [0..\longitud {keys(preg)}) ( (\longitud {\comp {h}{h \selec
trivias (g), k \in keywords(h)}} == 1) \ylogico \\ 
(mismosParticipantesSinU(dameTrivia(preg,k),dameTrivia(g,k),k,u)) \ylogico \\ 
(mismosGanadoresSinU(dameTrivia(preg,k),dameTrivia(g,k),k,u)) \ylogico \\ 
(preguntas(dameTrivia(preg,k)) == preguntas(dameTrivia(g,k))) \ylogico \\ 
(mismos(keywords(dameTrivia(preg,k)), keywords(dameTrivia(g,k)))) \ylogico \\
(losDemasMismasPreguntas(dameTrivia(preg,k),dameTrivia(g,k), u)) \ylogico \\ 
(losDemasMismosPuntajes(dameTrivia(preg,k),dameTrivia(g,k), u)) )  \\ \ylogico
texto(result)==\!''Listo,\ ya\ te\ borramos!.'' }
\end{aux}

\medskip
	
\begin{aux}{OkBajaTrivia}{g,preg:Gateway, k:Keyword, u:Usuario,
result:SMS}{Bool}{\\ ((\forall h \selec trivias(preg), k \not\in keywords(h))
(\exists m \selec trivias(g))h==m) \\ \ylogico ((\exists n \selec trivias(g)) (k
\in keywords(n)) \ylogico \\ 
(mismosParticipantesSinU(dameTrivia(preg,k),n,k,u)) \ylogico \\
(mismosGanadoresSinU(dameTrivia(preg,k),n,k,u)) \ylogico \\
(preguntas(dameTrivia(preg,k)) == preguntas(n)) \ylogico \\ (mismos(keywords(dameTrivia(preg,k)), keywords(dameTrivia(g,k)))) \ylogico
\\ (losDemasMismasPreguntas(dameTrivia(preg,k),n,u)) \ylogico \\ 
(losDemasMismosPuntajes(dameTrivia(preg,k),n,u)))
\\ \ylogico texto(result)==\!''Listo,\ ya\ te\ borramos!.''
}
\end{aux}

\medskip

\begin{aux}{OkRankingTrivia}{g,preg:Gateway, k:Keyword, u:Usuario,
result:SMS}{Bool}{\\ mismos(trivias(preg), trivias(g))
\\ \ylogico ''Tu\ posicion\ en\ la\ trivia\ es\ '' \masmas
intToString(auxPosicionEnT(dameTrivia(g,k),u)) == texto(result)}
\end{aux} 

\medskip

\begin{aux}{keys}{g: Gateway}{[Keywords]}{
\comp{keywords(t)_0}{t \selec trivias(g)}}

\end{aux}


\begin{aux}{mismosParticipantesSinU}{g,preg: Gateway, k: Keyword, u:
Usuarios}{Bool}{ \\ mismos ( \comp{p}{p \selec
participantes(dameTrivia(preg,k)), u \neq p)}, participantes(dameTrivia(g,k)))
}
\end{aux}

\begin{aux}{mismosGanadoresSinU}{g,preg: Gateway, k: Keyword, u:
Usuarios}{Bool}{ \\ mismos ( \comp{p}{p \selec ganadores(dameTrivia(preg,k)), u
\neq p)}, ganadores(dameTrivia(g,k))
}
\end{aux}

% Aprobado por Lea Domingo 25 septiembre. Importante : Cambi� un par de cosas .
% Agregu� un par�metro (keyword) a algunas de las funciones auxiliares, y cambi�
% otra para no romper un invariante. El que tenga ganas despu�s compare con la
% versi�n anterior a ver qu� opinan. AH, y aunque no lo crean, verifiqu� todos
% los par�ntesis, as� que traten de no cambiarlos porque creo que est�n bien. O
% mejor dicho revisen antes de hacerlo ! 
